X:Type, x:chain_config(), head, tail:X, pred:(IdX), succ:(IdX).
chain_config_ind(x;head;tail;id.pred(id);id,num.succ(id,num))  X 

latex

Definitions	s = t, t  T, x:AB(x), x:A. B(x), x. t(x), Id, , t.2, Type, x.A(x), t.1, f(a), x(s1,s2), x:A  B(x), x(s), left + right, chain_config(), chain_config_ind(x;head;tail;id.pred(id);id,num.succ(id;num)), a:A fp B(a), strong-subtype(A;B), P  Q
Lemmas	chain config wf, member wf, pi1 wf, nat wf, Id wf, pi2 wf